(declare-sort S0 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const r0 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const r10 Real)
(declare-const r11 Real)
(declare-const r12 Real)
(declare-const r13 Real)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const r14 Real)
(declare-const r15 Real)
(assert v3)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const r16 Real)
(declare-const S0-0 S0)
(assert (= (and (<= (/ 0.9 r7) r13) (> r12 31 0.9)) v2 (<= r3 r5 0.8412)))
(declare-const S0-1 S0)
(declare-const r17 Real)
(assert (xor (<= (/ 0.9 r7) r13) v10 v5 v1 v6 (xor v3 v15 v3 (<= r3 r5 0.8412) (= v14 v4 (<= (/ 0.9 r7) r13) v12 v1 (<= (/ 0.9 r7) r13) v10 v11) (> r12 31 0.9) v8 (< r12 (+ r3 r8 r5 r11) r12) (< r12 (+ r3 r8 r5 r11) r12) v2 (> r12 31 0.9)) (= (and (<= (/ 0.9 r7) r13) (> r12 31 0.9)) v2 (<= r3 r5 0.8412)) (< r12 (+ r3 r8 r5 r11) r12) (<= r3 r5 0.8412) (<= r8 0.8412 r3 r15) (< r12 (+ r3 r8 r5 r11) r12)))
(declare-const v17 Bool)
(declare-const r18 Real)
(declare-const v18 Bool)
(assert (<= (/ 0.9 r7) r13))
(declare-const v19 Bool)
(declare-const r19 Real)
(declare-const S0-2 S0)
(declare-const v20 Bool)
(assert (=> v12 v9))
(declare-const S0-3 S0)
(declare-const v21 Bool)
(assert (not (= r14 0.9 r0 r15)))
(assert v2)
(check-sat)
